(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
head(Cons(x, xs)) → x
e(Cons(F, Nil), b) → False
e(Cons(T, Nil), b) → False
e(Cons(B, Nil), b) → False
e(Cons(A, Nil), b) → e[Match][Cons][Ite][True][Match](A, Nil, b)
e(Cons(F, Cons(x, xs)), b) → False
e(Cons(T, Cons(x, xs)), b) → False
e(Cons(B, Cons(x, xs)), b) → False
e(Cons(A, Cons(x, xs)), b) → False
equal(F, F) → True
equal(F, T) → False
equal(F, B) → False
equal(F, A) → False
equal(T, F) → False
equal(T, T) → True
equal(T, B) → False
equal(T, A) → False
equal(B, F) → False
equal(B, T) → False
equal(B, B) → True
equal(B, A) → False
equal(A, F) → False
equal(A, T) → False
equal(A, B) → False
equal(A, A) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
e(Nil, b) → False
t(x, y) → t[Ite](e(x, y), x, y)
r(x, y) → r[Ite](e(x, y), x, y)
q(x, y) → q[Ite](e(x, y), x, y)
p(x, y) → p[Ite](e(x, y), x, y)
goal(x, y) → q(x, y)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))
q[Ite](False, x, Cons(F, Cons(T, xs))) → False
q[Ite](False, x, Cons(F, Cons(B, xs))) → False
q[Ite](False, x, Cons(F, Cons(A, xs))) → False
q[Ite](False, x, Cons(T, Cons(F, xs))) → False
q[Ite](False, x, Cons(T, Cons(T, xs))) → False
q[Ite](False, x, Cons(T, Cons(B, xs))) → False
q[Ite](False, x, Cons(T, Cons(A, xs))) → False
q[Ite](False, x, Cons(B, Cons(F, xs))) → False
q[Ite](False, x, Cons(B, Cons(T, xs))) → False
q[Ite](False, x, Cons(B, Cons(B, xs))) → False
q[Ite](False, x, Cons(B, Cons(A, xs))) → False
q[Ite](False, x, Cons(A, Cons(F, xs))) → False
q[Ite](False, x, Cons(A, Cons(T, xs))) → False
q[Ite](False, x, Cons(A, Cons(B, xs))) → False
q[Ite](False, x, Cons(A, Cons(A, xs))) → False
q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))
r[Ite](False, x, Cons(T, xs)) → False
r[Ite](False, x, Cons(B, xs)) → False
r[Ite](False, x, Cons(A, xs)) → False
p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))
p[Ite](False, x, Cons(T, xs)) → False
p[Ite](False, x, Cons(B, xs)) → False
p[Ite](False, x, Cons(A, xs)) → False
q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))
t[Ite](False, x, y) → True
t[Ite](True, x, y) → True
r[Ite](True, x, y) → True
q[Ite](True, x, y) → True
q[Ite][False][Ite](False, x, y) → False
p[Ite](True, x, y) → True
Rewrite Strategy: INNERMOST
(1) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
e/1
e[Match][Cons][Ite][True][Match]/0
e[Match][Cons][Ite][True][Match]/1
e[Match][Cons][Ite][True][Match]/2
t/1
t[Ite]/1
t[Ite]/2
q[Ite][False][Ite][True][Ite]/1
q[Ite][False][Ite][True][Ite]/2
r[Ite][False][Ite][True][Ite]/1
r[Ite][False][Ite][True][Ite]/2
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
head(Cons(x, xs)) → x
e(Cons(F, Nil)) → False
e(Cons(T, Nil)) → False
e(Cons(B, Nil)) → False
e(Cons(A, Nil)) → e[Match][Cons][Ite][True][Match]
e(Cons(F, Cons(x, xs))) → False
e(Cons(T, Cons(x, xs))) → False
e(Cons(B, Cons(x, xs))) → False
e(Cons(A, Cons(x, xs))) → False
equal(F, F) → True
equal(F, T) → False
equal(F, B) → False
equal(F, A) → False
equal(T, F) → False
equal(T, T) → True
equal(T, B) → False
equal(T, A) → False
equal(B, F) → False
equal(B, T) → False
equal(B, B) → True
equal(B, A) → False
equal(A, F) → False
equal(A, T) → False
equal(A, B) → False
equal(A, A) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
e(Nil) → False
t(x) → t[Ite](e(x))
r(x, y) → r[Ite](e(x), x, y)
q(x, y) → q[Ite](e(x), x, y)
p(x, y) → p[Ite](e(x), x, y)
goal(x, y) → q(x, y)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))))
q[Ite](False, x, Cons(F, Cons(T, xs))) → False
q[Ite](False, x, Cons(F, Cons(B, xs))) → False
q[Ite](False, x, Cons(F, Cons(A, xs))) → False
q[Ite](False, x, Cons(T, Cons(F, xs))) → False
q[Ite](False, x, Cons(T, Cons(T, xs))) → False
q[Ite](False, x, Cons(T, Cons(B, xs))) → False
q[Ite](False, x, Cons(T, Cons(A, xs))) → False
q[Ite](False, x, Cons(B, Cons(F, xs))) → False
q[Ite](False, x, Cons(B, Cons(T, xs))) → False
q[Ite](False, x, Cons(B, Cons(B, xs))) → False
q[Ite](False, x, Cons(B, Cons(A, xs))) → False
q[Ite](False, x, Cons(A, Cons(F, xs))) → False
q[Ite](False, x, Cons(A, Cons(T, xs))) → False
q[Ite](False, x, Cons(A, Cons(B, xs))) → False
q[Ite](False, x, Cons(A, Cons(A, xs))) → False
q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)))
r[Ite](False, x, Cons(T, xs)) → False
r[Ite](False, x, Cons(B, xs)) → False
r[Ite](False, x, Cons(A, xs)) → False
p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))
p[Ite](False, x, Cons(T, xs)) → False
p[Ite](False, x, Cons(B, xs)) → False
p[Ite](False, x, Cons(A, xs)) → False
q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)))
t[Ite](False) → True
t[Ite](True) → True
r[Ite](True, x, y) → True
q[Ite](True, x, y) → True
q[Ite][False][Ite](False, x, y) → False
p[Ite](True, x, y) → True
Rewrite Strategy: INNERMOST
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
r(Cons(F, Nil), Cons(F, xs5015_0)) →+ r[Ite][False][Ite][True][Ite](and(q(Cons(F, Nil), xs5015_0), r(Cons(F, Nil), xs5015_0)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1].
The pumping substitution is [xs5015_0 / Cons(F, xs5015_0)].
The result substitution is [ ].
(4) BOUNDS(n^1, INF)